$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} .
\\[0ex]($\uparrow$$x$ changed before $e$) $\Rightarrow$ (($x$ when $e$) = ($x$ after (last change to $x$ before $e$)) $\in$ $T$)